Problem:
 active(g(X)) -> mark(h(X))
 active(c()) -> mark(d())
 active(h(d())) -> mark(g(c()))
 proper(g(X)) -> g(proper(X))
 proper(h(X)) -> h(proper(X))
 proper(c()) -> ok(c())
 proper(d()) -> ok(d())
 g(ok(X)) -> ok(g(X))
 h(ok(X)) -> ok(h(X))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {9,8,7,6,5}
   transitions:
    ok3(124) -> 125*
    top1(62) -> 63*
    d3() -> 124*
    active1(80) -> 81*
    active1(86) -> 87*
    active1(88) -> 89*
    active1(78) -> 79*
    top4(132) -> 133*
    proper1(70) -> 71*
    proper1(72) -> 73*
    proper1(64) -> 65*
    proper1(61) -> 62*
    active4(131) -> 132*
    ok1(44) -> 45*
    ok1(26) -> 27*
    ok1(16) -> 17*
    ok1(18) -> 19*
    h1(52) -> 53*
    h1(54) -> 55*
    h1(46) -> 47*
    h1(43) -> 44*
    g1(25) -> 26*
    g1(34) -> 35*
    g1(36) -> 37*
    g1(28) -> 29*
    d1() -> 10*
    c1() -> 16*
    mark1(10) -> 11*
    top2(93) -> 94*
    active0(2) -> 5*
    active0(4) -> 5*
    active0(1) -> 5*
    active0(3) -> 5*
    active2(104) -> 105*
    active2(98) -> 99*
    g0(2) -> 7*
    g0(4) -> 7*
    g0(1) -> 7*
    g0(3) -> 7*
    proper2(92) -> 93*
    mark0(2) -> 1*
    mark0(4) -> 1*
    mark0(1) -> 1*
    mark0(3) -> 1*
    ok2(110) -> 111*
    h0(2) -> 8*
    h0(4) -> 8*
    h0(1) -> 8*
    h0(3) -> 8*
    d2() -> 106*
    c0() -> 2*
    mark2(106) -> 107*
    d0() -> 3*
    top3(118) -> 119*
    proper0(2) -> 6*
    proper0(4) -> 6*
    proper0(1) -> 6*
    proper0(3) -> 6*
    active3(122) -> 123*
    ok0(2) -> 4*
    ok0(4) -> 4*
    ok0(1) -> 4*
    ok0(3) -> 4*
    proper3(117) -> 118*
    top0(2) -> 9*
    top0(4) -> 9*
    top0(1) -> 9*
    top0(3) -> 9*
    1 -> 86,70,52,34
    2 -> 78,61,43,25
    3 -> 88,72,54,36
    4 -> 80,64,46,28
    10 -> 92,18
    11 -> 79,62,5
    16 -> 98*
    17 -> 62,6
    18 -> 104*
    19 -> 73,62,6
    27 -> 29,26,7
    29 -> 26*
    35 -> 26*
    37 -> 26*
    45 -> 47,44,8
    47 -> 44*
    53 -> 44*
    55 -> 44*
    63 -> 9*
    65 -> 62*
    71 -> 62*
    73 -> 62*
    79 -> 62*
    81 -> 62*
    87 -> 62*
    89 -> 62*
    94 -> 63,9
    99 -> 93*
    105 -> 93*
    106 -> 117,110
    107 -> 99,93
    110 -> 122*
    111 -> 93*
    119 -> 94,63
    123 -> 118*
    124 -> 131*
    125 -> 118*
    133 -> 119,94
  problem:
   
  Qed